|
ISP ("In-situ Partial Order") is a tool for the formal verification of MPI programs developed within the School of Computing at the University of Utah. Like model checkers, such as SPIN, ISP verifies the complete state space of a system for a set of safety properties. However, unlike model checkers, ISP performs ''code level verification''. This means that the tool verifies all ''relevant interleavings'' of a concurrent program by replaying the actual program code ''without'' building verification models. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool.〔Patrice Godefroid, ''Model Checking for Programming Languages using VeriSoft'' (POPL 1997 )〕 Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST. Relevant interleavings are computed using a customized ''dynamic partial order reduction''〔Cormac Flanagan and Patrice Godefroid, ''Dynamic partial-order reduction for model checking software,'', (POPL 2005 ), pp. 110-121, ACM, ISBN 1-58113-830-X〕 algorithm called ''POE''.〔Sarvani Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby, ``Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings,'' Computer Aided Verification ((CAV 2008) ), pp. 66-79, LNCS 5123. 〕 ISP has been used to successfully verify up to 14,000 lines of MPI/C code for deadlocks and assertion violations. It currently supports over 60 MPI 2.1 functions, and has been tested with MPICH2, OpenMPI,and Microsoft MPI libraries. ISP is available for download for linux and Mac OS X; as a Visual Studio plugin for running under Windows, and as an Eclipse plugin.. ==References== 〔 Anh Vo, Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur, ``Formal Verification of Practical MPI Programs,'' (PPoPP 2009 ) Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby, ``Scheduling Considerations for Building Dynamic Verification Tools for MPI,'' Parallel and Distributed Systems - Testing and Debugging ((PADTAD-VI) ), Seattle, WA, July, 2008. Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, ``Implementing Efficient Dynamic Formal Verification Methods for MPI Programs,'' Recent Advances in Parallel Virtual Machine and Message Passing Interface ((EuroPVM/MPI 2008) ), Dublin, Ireland, 2008, LNCS 5205, pp. 248–256. Sarvani Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, and Robert M. Kirby, ``ISP: A Tool for Model Checking MPI Programs,'' Principles and Practices of Parallel Programming ((PPoPP 2008) ), Salt Lake City, February 2008, pp. 285–286. Salman Pervez, Robert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, ``Practical Model Checking Methods for Verifying Correctness of MPI Programs,'' Recent Advances in Parallel Virtual Machine and Message Passing Interface ((PDF) ) (EuroPVM/MPI), Paris, 344—353, LNCS 4757, France, September 30 - October 3, 2007 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「ISP Formal Verification Tool」の詳細全文を読む スポンサード リンク
|